(set-logic ALL)
(set-info :status sat)
(declare-fun A () (Bag Int))
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
(assert (bag.subbag A B))
(assert (bag.subbag B A))
(assert (= (bag.count x A) x))
(assert (= (bag.count y A) x))
(assert (distinct x y))
(assert (= (bag.count x B) (+ 1 y)))
(check-sat)